package rules;
import scala.{Symbol => ScalaSymbol}

trait Narrowing {
  trait Term
  
  case class Symbol(name: String) extends Term {
    assert(!Character.isUpperCase(name.charAt(0)))
  }
  
  case class Variable(name: String) extends Term {
    assert(Character.isUpperCase(name.charAt(0)))
  }
  
  implicit def scalaSymbolToTerm(s: ScalaSymbol): Term 
  = if (Character.isUpperCase(s.name.charAt(0))) Variable(s.name) else Symbol(s.name)
  
  trait Rule
}


trait Syntax {
  trait Term
  trait Type
}

class Rules {
  
  /*of/new : (new T) of T
  <- expands T SelfT Mems           % T must expand to a list of members with self type SelfT
  % (T is not necessarily equivalent to a structural type -- e.g., nominal type binding)
<- T < SelfT                      % subtyping ignores abstract vs concrete members
  % T may have abstract type/value members to model polymorphic lambda's as values

<- ({selfv} {dof: selfv of SelfT} WF@mems (Mems selfv)). % assuming a self variable of the right type, 
              % the members must be well-formed (also checks there are not duplicates)
*/
  
  // TODO: use singleton typess to model Twelf's types
  case class Judgement(jdgs: Judgement*) {
    def -> (conclude: Judgement) = Rule(this, conclude)
    def `<-` (conclude: Judgement) = Rule(conclude, this)    
  }
  
  case class Rule(jdgs: Judgement*) {
    def -> (conclude: Judgement) = Rule( (jdgs.elements.toList ::: List(conclude)): _*)
    def `<-` (hyp: Judgement) = Rule( (hyp :: jdgs.elements.toList): _*)
  }
  
  val tm = Judgement()
  val tp = Judgement()
  def new_ = tp -> tm
  def of = Judgement(tm, tp)
  
  /*def of(tm: V[Term], tp: V[Type])
  def of_new = conclude(of(tm_new(`T), `T))
    <- expands(`T, `SelfT, `Mems)
    <- <(`T, `SelfT)
    <- assume(`selfv, `*/

}
